T:Type, L:T List, x:T, i, j:{1..(||L||+1)}. swap(x.L;i;j) = (x.swap(L;i-1;j-1)) 

latex

Definitions	, t  T, x:A. B(x), swap(L;i;j), ||as||, Prop, ij, {i..j}, P  Q, False, A, P & Q, AB, i  j < k, P  Q, P  Q, {T}, SQType(T), P  Q, Dec(P), hd(l), i<j, ij, l[i], b, b, , Unit, if b t else f fi, i=j, (i, j), True, T
Lemmas	squash wf, true wf, select cons tl, select wf, bool wf, ifthenelse wf, eq int wf, eqtt to assert, eqff to assert, iff transitivity, assert of bnot, not functionality wrt iff, assert of eq int, bnot wf, not wf, assert wf, swap select, le wf, decidable int equal, add functionality wrt eq, swap length, int seg wf, list extensionality, length cons, non neg length, swap wf, length wf1, nat wf